|
Ein großes Problem bei der gemeinsamen Erstellung von Dokumenten
durch mehrere Personen betrifft die Konsistenz der Daten, denn jeder
sollte beliebige Änderungen vornehmen können. Dies gilt in
besonderem Maß, wenn Benutzer mit mobilen Endgeräten beteiligt
sind, welche nicht permanent mit den Datenservern verbunden sind und
somit die meiste Zeit Offline arbeiten. D.h. die Daten werden lokal
bearbeitet und Änderungen eher abschnittsweise, auf einmal in das
gemeinsame Dokument eingebracht. Um die dabei nicht zwangsweise
entstehenden Inkonsistenzen zu kontrollieren und zu beheben, wurden
bereits eine Reihe von Protokollen zur Konsistenzerhaltung (z.B.
Grove, 2-Phasen-Sperren) vorgeschlagen.
Diese, mit zunehmender Komplexität, verwendeten Protokolle
bestimmen in großem Maß den reibungslosen Ablauf bei der
gemeinsamen Erstellung/Bearbeitung von Dokumenten. Deren
Zuverlässigkeit scheint eine unabdingbare Forderung zu sein. Der
Nachweis der "fehlerfreien Funktion"(Verifikation) ist
jedoch ein sehr schwieriges Unterfangen.
Die am häufigsten verwendeten Verifikationstechniken sind Test
(z.B. Blackbox- und Glasboxtest) und Simulation. Diese Verfahren
sind jedoch sehr aufwändig und garantieren keine 100%ige
Fehlerfreiheit.
Anfang der 80er Jahre wurde eine Methode entwickelt, welche es
erlaubt, die logische Struktur komplexer Systeme/Protokolle
vollautomatisch zu analysieren und den Nachweis der gestellten
Anforderungen zu erbringen. Diese Technik wird Model Checking
genannt und ist Grundbaustein moderner Verifikationswerkzeuge (z.B.
Spin, Verisoft, UPPAAL, ...). Diese Werkzeuge erlauben die
Modellierung und Verifikation von parallelen Systemen,
Kommunikationsprotokollen und u.v.m.
Dabei werden die unterschiedlichsten Methoden verwendet.
Beispielsweise besitzt Spin eine eigene Spezifikationssprache, mit
welcher z.B. Kommunikationsprotokolle nachgebildet werden können,
wogegen Verisoft auf dem Sourcecode arbeitet und die gestellten
Forderungen direkt im zu überprüfenden System/Protokoll definiert
werden können.
Um die an ein zu verifizierendes System gestellten Forderungen
präzise formulieren und überprüfen (z.B. Finden von Deadlocks
(Verklemmungen) und "unerreichbaren" Unterroutinen) zu
können, verwenden die einzelnen Werkzeuge gesonderte oder
integrierte Spezifikationsformalismen (z.B. LTL, CTL).
|